『Programming in Martin-Löf ’s type theory』目次
Contents
内容
1 Introduction 1
1 はじめに 1
1.1 Using type theory for programming 3
1.1 プログラミングに型論を使用する 3
1.2 Constructive mathematics 6
1.2 構成的数学 6
1.3 Different formulations of type theory 6
1.3 型論の異なる定式化 6
1.4 Implementations of programming logics 8
1.4 プログラミングロジックの実装 8
2 The identification of sets, propositions and specifications 9
2 集合、命題、仕様の識別 9
2.1 Propositions as sets 9
2.1 集合としての命題 9
2.2 Propositions as tasks and specifications of programs 12
2.2 プログラムのタスクと仕様としての命題 12
3 Expressions and definitional equality 13
3 式と定義の等価性 13
3.1 Application 13
3.1 適用 13
3.2 Abstraction 14
3.2 抽象化 14
3.3 Combination 15
3.3 組み合わせ 15
3.4 Selection 16
3.4 セレクション16
3.5 Combinations with named components 16
3.5 名前付きコンポーネントとの組み合わせ 16
3.6 Arities 17
3.6 アリティ 17
3.7 Definitions 19
3.7 定義 19
3.8 Definition of what an expression of a certain arity is 19
3.8 あるアリティの表現が何であるかの定義 19
3.9 Definition of equality between two expressions 20
3.9 2つの式間の等価性の定義 20
4 The semantics of the judgement forms 25
4 判断形式の意味論 25
4.1 Categorical judgements 27
4.1 カテゴリー判断 27
4.1.1 What does it mean to be a set? 27
4.1.1 セットとはどういう意味ですか?27
4.1.2 What does it mean for two sets to be equal? 28
4.1.2 2つのセットが等しいとはどういう意味ですか?28
4.1.3 What does it mean to be an element in a set? 28
4.1.3 集合内の要素であるとはどういう意味ですか?28
4.1.4 What does it mean for two elements to be equal in a set? 29
4.1.4 セット内の 2 つの要素が等しいとはどういう意味ですか?29
4.1.5 What does it mean to be a proposition? 29
4.1.5 命題であるとはどういう意味ですか?29
4.1.6 What does it mean for a proposition to be true? 29
4.1.6 命題が真であるとはどういう意味ですか?29
4.2 Hypothetical judgements with one assumption 29
4.2 1つの仮定による仮説的判断 29
4.2.1 What does it mean to be a set under an assumption? 30
4.2.1 仮定の下で集合であるとはどういう意味ですか?30
4.2.2 What does it mean for two sets to be equal under an assumption? 30
4.2.2 仮定の下で2つのセットが等しいとはどういう意味ですか?30
4.2.3 What does it mean to be an element in a set under an assumption? 30
4.2.3 仮定の下で集合内の要素であるとはどういう意味ですか?30
4.2.4 What does it mean for two elements to be equal in a set under an assumption? 31
4.2.4 仮定の下で、2つの要素が集合内で等しいとはどういう意味ですか?31
4.2.5 What does it mean to be a proposition under an assumption? 31
4.2.5 仮定の下で命題であるとはどういう意味ですか?31
4.2.6 What does it mean for a proposition to be true under an assumption? 31
4.2.6 仮定の下で命題が真であるとはどういう意味ですか?31
4.3 Hypothetical judgements with several assumptions 31
4.3 いくつかの仮定による仮説的判断 31
4.3.1 What does it mean to be a set under several assumptions? 31
4.3.1 いくつかの仮定の下で集合であるとはどういう意味ですか?31
4.3.2 What does it mean for two sets to be equal under several assumptions? 32
4.3.2 いくつかの仮定の下で2つのセットが等しいとはどういう意味ですか?32
4.3.3 What does it mean to be an element in a set under several assumptions? 32
4.3.3 いくつかの仮定の下で集合内の要素であるとはどういう意味ですか?32
4.3.4 What does it mean for two elements to be equal in a set under several assumptions? 33
4.3.4 いくつかの仮定の下で、2つの要素が集合内で等しいとはどういう意味ですか?33
4.3.5 What does it mean to be a proposition under several assumptions? 33
4.3.5 いくつかの仮定の下で命題であるとはどういう意味ですか?33
4.3.6 What does it mean for a proposition to be true under several assumptions? 33
4.3.6 いくつかの仮定の下で命題が真であるとはどういう意味ですか?33
5 General rules 35
5 一般規則 35
5.1 Assumptions 37
5.1 仮定 37
5.2 Propositions as sets 37
5.2 集合としての命題 37
5.3 Equality rules 37
5.3 平等のルール 37
5.4 Set rules 38
5.4 ルールを設定する 38
5.5 Substitution rules 38
5.5 代替ルール 38
6 Enumeration sets 41
6 列挙セット 41
6.1 Absurdity and the empty set 43
6.1 不条理と空の集合 43
6.2 The one-element set and the true proposition 43
6.2 1要素集合と真命題43
6.3 The set Bool 44
6.3 セット Bool 44
7 Cartesian product of a family of sets 47
7 セットファミリーのデカルト積 47
7.1 The formal rules and their justification 49
7.1 正式な規則とその正当化 49
7.2 An alternative primitive non-canonical form 51
7.2 代替プリミティブ非正規形式 51
7.3 Constants defined in terms of the Π set 53
7.3 Π集合53で定義される定数
7.3.1 The universal quantifier (∀) 53
7.3.1 普遍的な量指定子(∀) 53
7.3.2 The function set (→) 53
7.3.2 関数セット(→)53
7.3.3 Implication (⊃) 54
7.3.3 含意 (⊃) 54
8 Equality sets 57
8 等価セット 57
8.1 Intensional equality 57
8.1 内在的等価性 57
8.2 Extensional equality 60
8.2 拡張等式 60
8.3 η-equality for elements in a Π set 62
8.3 Π集合内の要素のη等式 62
9 Natural numbers 63
9 自然数 63
10 Lists 67
10 リスト 67
11 Cartesian product of two sets 73
11 2セットのデカルト積 73
11.1 The formal rules 73
11.1 正式な規則 73
11.2 Extensional equality on functions 77
11.2 関数の拡張等価性 77
12 Disjoint union of two sets 79
12 2つのセットの不結合 79
13 Disjoint union of a family of sets 81
13 集合の族の不結合 81
14 The set of small sets (The first universe) 83
14 小集合(最初の宇宙) 83
14.1 Formal rules 83
14.1 正式なルール 83
14.2 Elimination rule 91
14.2 排除規則 91
15 Well-orderings 97
15 井戸の順序付け 97
15.1 Representing inductively defined sets by well-orderings 101
15.1 井戸順序付けによる帰納的に定義された集合の表現 101
16 General trees 103
16 一般木 103
16.1 Formal rules 104
16.1 正式な規則 104
16.2 Relation to the well-order set constructor 106
16.2 井戸集合コンストラクタ106との関係
16.3 A variant of the tree set constructor 108
16.3 ツリーセットコンストラクタ108の変種
16.4 Examples of different tree sets 108
16.4 異なるツリーセットの例 108
16.4.1 Even and odd numbers 108
16.4.1 偶数と奇数 108
16.4.2 An infinite family of sets 110
16.4.2 集合の無限族 110
II Subsets 111
II サブセット 111
17 Subsets in the basic set theory 113
17 基本集合論のサブセット 113
18 The subset theory 117
18 部分集合理論 117
18.1 Judgements without assumptions 117
18.1 仮定のない判断 117
18.1.1 What does it mean to be a set? 118
18.1.1 セットとはどういう意味ですか?118
18.1.2 What does it mean for two sets to be equal? 118
18.1.2 2つのセットが等しいとはどういう意味ですか?118
18.1.3 What does it mean to be an element in a set? 118
18.1.3 集合内の要素であるとはどういう意味ですか?118
18.1.4 What does it mean for two elements to be equal in a set? 119
18.1.4 2つの要素が集合内で等しいとはどういう意味ですか?119
18.1.5 What does it mean to be a proposition? 119
18.1.5 命題であるとはどういう意味ですか?119
18.1.6 What does it mean for a proposition to be true? 119
18.1.6 命題が真であるとはどういう意味ですか?119
18.2 Hypothetical judgements 119
18.2 仮説上の判断 119
18.2.1 What does it mean to be a set under assumptions? 120
18.2.1 仮定の下で集合であるとはどういう意味ですか?120
18.2.2 What does it mean for two sets to be equal under assumptions? 120
18.2.2 仮定の下で2つのセットが等しいとはどういう意味ですか?120
18.2.3 What does it mean to be an element in a set under assumptions? 121
18.2.3 仮定の下で集合内の要素であるとはどういう意味ですか?121
18.2.4 What does it mean for two elements to be equal in a set under assumptions? 121
18.2.4 仮定の下で集合内で2つの要素が等しいとはどういう意味ですか?121
18.2.5 What does it mean to be a proposition under assumptions? 122
18.2.5 仮定の下で命題であるとはどういう意味ですか?122
18.2.6 What does it mean for a proposition to be true under assumptions? 122
18.2.6 仮定の下で命題が真であるとはどういう意味ですか?122
18.3 General rules in the subset theory 122
18.3 部分集合理論の一般規則 122
18.4 The propositional constants in the subset theory 124
18.4 部分集合理論の命題定数 124
18.4.1 The logical constants 124
18.4.1 論理定数 124
18.4.2 The propositional equality 125
18.4.2 命題等式 125
18.5 Subsets formed by comprehension 126
18.5 理解によって形成されるサブセット 126
18.6 The individual set formers in the subset theory 127
18.6 部分集合理論における個々の集合形成者 127
18.6.1 Enumeration sets 127
18.6.1 列挙セット 127
18.6.2 Equality sets 128
18.6.2 等価セット 128
18.6.3 Natural numbers 128
18.6.3 自然数 128
18.6.4 Cartesian product of a family of sets 128
18.6.4 セットファミリーのデカルト積 128
18.6.5 Disjoint union of two sets 130
18.6.5 2 セットの不結合 130
18.6.6 Disjoint union of a family of sets 130
18.6.6 集合の族の不結合 130
18.6.7 Lists 131
18.6.7 リスト 131
18.6.8 Well-orderings 131
18.6.8 井戸の順序付け 131
18.7 Subsets with a universe 131
18.7 ユニバース131を持つサブセット
III Monomorphic sets 135
III モノモルフィックセット 135
19 Types 137
19種類 137
19.1 Types and objects 138
19.1 型とオブジェクト 138
19.2 The types of sets and elements 139
19.2 セットと要素の種類 139
19.3 Families of types 139
19.3 タイプ139のファミリー
19.4 General rules 141
19.4 一般規則 141
19.5 Assumptions 142
19.5 仮定 142
19.6 Function types 143
19.6 関数型 143
20 Defining sets in terms of types 147
20 型147の観点からセットを定義する
20.1 Π sets 148
20.1 πセット 148
20.2 Σ sets 149
20.2 Σセット 149
20.3 Disjoint union 150
20.3 不結合 150
20.4 Equality sets 150
20.4 等価セット 150
20.5 Finite sets 151
20.5 有限集合 151
20.6 Natural numbers 151
20.6 自然数 151
20.7 Lists 152
20.7 リスト 152
IV Examples 153
IV 事例 153
21 Some small examples 155
21 いくつかの小さな例 155
21.1 Division by 2 155
21.1 2で割る 155
21.2 Even or odd 159
21.2 偶数または奇数 159
21.3 Bool has only the elements true and false 160
21.3 Bool には true と false の要素しかありません 160
21.4 Decidable predicates 162
21.4 決定可能な述語 162
21.5 Stronger elimination rules 163
21.5 より強力なエリミネーションルール 163
22 Program derivation 167
22 プログラム派生 167
22.1 The program derivation method 167
22.1 プログラム導出方法 167
22.1.1 Basic tactics 168
22.1.1 基本的な戦術 168
22.1.2 Derived tactics 170
22.1.2 派生戦術 170
22.2 A partitioning problem 171
22.2 パーティションの問題 171
23 Specification of abstract data types 179
23 抽象データ型の指定 179
23.1 Parameterized modules 181
23.1 パラメータ化されたモジュール 181
23.2 A module for sets with a computable equality 182
23.2 計算可能な等式を持つ集合のモジュール 182
A Constants and their arities 197
A 定数とそのアリティ 197
A.1 Primitive constants in the set theory 197
A.1 集合論における原始定数 197
A.2 Set constants 198
A.2 定数を設定する 198
B Operational semantics 199
B 操作セマンティクス 199
B.1 Evaluation rules for noncanonical constants 200
B.1 非正準定数の評価ルール 200
(空白)